Nuprl Lemma : cond_rel_implies_wf 4,23

T:Type, P:(TProp), R1R2:(TTProp). when PR1 => R2  Prop 
latex


Definitionswhen PR1 => R2, x:AB(x), P  Q, x f y, Prop, t  T

origin